\begin{tabbing}
$\forall$\=${\it poss}$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$),\+
\\[0ex]$R$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), $P$,
\\[0ex]$Q$:(possible{-}event\{i:l\}(${\it poss}$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\-\\[0ex]($\forall$$e$:possible{-}event\{i:l\}(${\it poss}$). $P$($e$) $\Rightarrow$ $Q$($e$))
\\[0ex]$\Rightarrow$ (\=$\forall$$e$:possible{-}event\=\{i:l\}\+\+
\\[0ex](${\it poss}$).
\-\\[0ex]es{-}knows\{i:l\}(${\it poss}$; $R$; $P$; $e$) $\Rightarrow$ es{-}knows\{i:l\}(${\it poss}$; $R$; $Q$; $e$))
\-
\end{tabbing}